a:, n:. (a < n)  ((a  n) = 0) 

latex

Up	int 2, int 2
Definitions	, t  T, P  Q, x:A. B(x), False, A, A  B, , P & Q, i  j < k, Div(a;n;q),
Lemmas	nat wf, nat plus wf, le wf, divide wf, div unique, div fun sat div nrel